// Copyright 2007-2009, Stanford University. All Rights Reserved.
// Copyright 2010-2011, Dependable Systems Lab, EPFL. All Rights Reserved.
// Copyright 2012, Google Inc. All Rights Reserved.
//
// Redistribution and use in source and binary forms, with or without
// modification, are permitted provided that the following conditions are
// met:
//
//     * Redistributions of source code must retain the above copyright
// notice, this list of conditions and the following disclaimers.
//     * Redistributions in binary form must reproduce the above
// copyright notice, this list of conditions and the following disclaimers
// in the documentation and/or other materials provided with the
// distribution.
//     * Neither the names of the klee Team, Stanford University, nor the
// names of its contributors may be used to endorse or promote
// products derived from the software without specific prior
// written permission. Neither the names of the Dependable Systems
// Laboratory, EPFL, nor the names of its contributors may be used to
// endorse or promote products derived from the software without prior
// written permission. Neither the names of Google Inc. nor the names of
// its contributors may be used to endorse or promote products derived from
// the software without specific prior written permission.
//
// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
// OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
// SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
// LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
// DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
// THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
// (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
// OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

#ifndef SRC_EXPR_PARSER_H_
#define SRC_EXPR_PARSER_H_

#include "expr/Expr.h"

#include <vector>
#include <string>

namespace llvm {
  class MemoryBuffer;
}

namespace seven_summits {
namespace expr {

using util::ref;

class ExprBuilder;
// These are the language types we manipulate.
typedef ref<Expr> ExprHandle;
typedef UpdateList VersionHandle;

/// Identifier - Wrapper for a uniqued string.
struct Identifier {
  const std::string Name;

public:
  Identifier(const std::string _Name) : Name(_Name) {}
};

// FIXME: Do we have a use for tracking source locations?

/// Decl - Base class for top level declarations.
class Decl {
public:
  enum DeclKind {
    ArrayDeclKind,
    ExprVarDeclKind,
    VersionVarDeclKind,
    QueryCommandDeclKind,

    DeclKindLast = QueryCommandDeclKind,
    VarDeclKindFirst = ExprVarDeclKind,
    VarDeclKindLast = VersionVarDeclKind,
    CommandDeclKindFirst = QueryCommandDeclKind,
    CommandDeclKindLast = QueryCommandDeclKind
  };

private:
  DeclKind Kind;

public:
  Decl(DeclKind _Kind);
  virtual ~Decl() {}

  /// getKind - Get the decl kind.
  DeclKind getKind() const { return Kind; }

  /// dump - Dump the AST node to stderr.
  virtual void dump() = 0;

  static bool classof(const Decl *) { return true; }
};

/// ArrayDecl - Array declarations.
///
/// For example:
///   array obj[] : w32 -> w8 = symbolic
///   array obj[32] : w32 -> w8 = [ ... ]
class ArrayDecl : public Decl {
public:
  /// Name - The name of this array.
  const Identifier *Name;

  /// Domain - The width of indices.
  const unsigned Domain;

  /// Range - The width of array contents.
  const unsigned Range;

  /// Root - The root array object defined by this decl.
  const Array *Root;

public:
  ArrayDecl(const Identifier *_Name, uint64_t _Size,
            unsigned _Domain, unsigned _Range,
            const Array *_Root)
    : Decl(ArrayDeclKind), Name(_Name),
      Domain(_Domain), Range(_Range),
      Root(_Root) {
  }

  virtual void dump();

  static bool classof(const Decl *D) {
    return D->getKind() == Decl::ArrayDeclKind;
  }
  static bool classof(const ArrayDecl *) { return true; }
};

/// VarDecl - Variable declarations, used to associate names to
/// expressions or array versions outside of expressions.
///
/// For example:
// FIXME: What syntax are we going to use for this? We need it.
class VarDecl : public Decl {
public:
  const Identifier *Name;

  static bool classof(const Decl *D) {
    return (Decl::VarDeclKindFirst <= D->getKind() &&
            D->getKind() <= Decl::VarDeclKindLast);
  }
  static bool classof(const VarDecl *) { return true; }
};

/// ExprVarDecl - Expression variable declarations.
class ExprVarDecl : public VarDecl {
public:
  ExprHandle Value;

  static bool classof(const Decl *D) {
    return D->getKind() == Decl::ExprVarDeclKind;
  }
  static bool classof(const ExprVarDecl *) { return true; }
};

/// VersionVarDecl - Array version variable declarations.
class VersionVarDecl : public VarDecl {
public:
  VersionHandle Value;

  static bool classof(const Decl *D) {
    return D->getKind() == Decl::VersionVarDeclKind;
  }
  static bool classof(const VersionVarDecl *) { return true; }
};

/// CommandDecl - Base class for language commands.
class CommandDecl : public Decl {
public:
  CommandDecl(DeclKind _Kind) : Decl(_Kind) {}

  static bool classof(const Decl *D) {
    return (Decl::CommandDeclKindFirst <= D->getKind() &&
            D->getKind() <= Decl::CommandDeclKindLast);
  }
  static bool classof(const CommandDecl *) { return true; }
};

/// QueryCommand - Query commands.
///
/// (query [ ... constraints ... ] expression)
/// (query [ ... constraints ... ] expression values)
/// (query [ ... constraints ... ] expression values objects)
class QueryCommand : public CommandDecl {
public:
  // FIXME: One issue with STP... should we require the FE to
  // guarantee that these are consistent? That is a cornerstone of
  // being able to do independence. We may want this as a flag, if
  // we are to interface with things like SMT.

  /// Constraints - The list of constraints to assume for this
  /// expression.
  const std::vector<ExprHandle> Constraints;

  /// Query - The expression being queried.
  ExprHandle Query;

  /// Values - The expressions for which counterexamples should be
  /// given if the query is invalid.
  const std::vector<ExprHandle> Values;

  /// Objects - Symbolic arrays whose initial contents should be
  /// given if the query is invalid.
  const std::vector<const Array*> Objects;

public:
  QueryCommand(const std::vector<ExprHandle> &_Constraints,
               ExprHandle _Query,
               const std::vector<ExprHandle> &_Values,
               const std::vector<const Array*> &_Objects
               )
    : CommandDecl(QueryCommandDeclKind),
      Constraints(_Constraints),
      Query(_Query),
      Values(_Values),
      Objects(_Objects) {}

  virtual void dump();

  static bool classof(const Decl *D) {
    return D->getKind() == QueryCommandDeclKind;
  }
  static bool classof(const QueryCommand *) { return true; }
};

/// Parser - Public interface for parsing a .pc language file.
class Parser {
protected:
  Parser();
public:
  virtual ~Parser();

  /// SetMaxErrors - Suppress anything beyond the first N errors.
  virtual void SetMaxErrors(unsigned N) = 0;

  /// GetNumErrors - Return the number of encountered errors.
  virtual unsigned GetNumErrors() const = 0;

  /// ParseTopLevelDecl - Parse and return a top level declaration,
  /// which the caller assumes ownership of.
  ///
  /// \return NULL indicates the end of the file has been reached.
  virtual Decl *ParseTopLevelDecl() = 0;

  /// CreateParser - Create a parser implementation for the given
  /// MemoryBuffer.
  ///
  /// \arg Name - The name to use in diagnostic messages.
  /// \arg MB - The input data.
  /// \arg Builder - The expression builder to use for constructing
  /// expressions.
  static Parser *Create(const std::string Name,
                        const llvm::MemoryBuffer *MB,
                        ExprBuilder *Builder);
};

}  // namespace expr
}  // namespace seven_summits

#endif  // SRC_EXPR_PARSER_H_
